<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | ThePRISMLanguage / Commands 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Introduction.html'>The PRISM Language</a> /
</p><h1>Commands</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<p>The behaviour of each module is described by <em>commands</em>,
comprising a <em>guard</em> and one or more <em>updates</em>.
The first command of module <code>M1</code> in our <a class='wikilink' href='Example1.html'>example</a> is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -&gt; <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
  <div class='sourceblocklink'><a href='Commands@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>The guard <code>x=0</code> indicates that this describes the behaviour of the module when the variable <code>x</code> has value 0.
The updates <code>(x'=0)</code> and <code>(x'=1)</code> and their associated probabilities state that the value of <code>x</code> will
remain at 0 with probability 0.8 and change to 1 with probability 0.2.
Note that the inclusion of updates in parentheses, e.g. <code>(x'=1)</code>, is essential.
While older versions of PRISM did not report the absence of parentheses as an error, newer versions do.
Note also that PRISM will complain if the probabilities on the right hand side of a command do not sum to one.
</p>
<p class='vspace'>The second command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">1</span> &amp; <span class="prismident">y</span>!=<span class="prismnum">2</span> -&gt; (<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
</div></div>
  <div class='sourceblocklink'><a href='Commands@action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>illustrates that guards can contain constraints on any variable, not just the ones in that module,
i.e. the behaviour of one module can depend on the state of another.
Updates, however, can only specify values for variables belonging to the module.
In general a module can <em>read</em> the variables of any other module, but only <em>write</em> to its own.
When a command comprises a single update with probability 1, the <code>1.0:</code> can be omitted,
as is done in the example above.
</p>
<p class='vspace'>If a module has more than one variable, updates describe the new value for each of them.
For example, if it had two variables <code>x1</code> and <code>x2</code>, a possible command would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>=<span class="prismnum">0</span> &amp; <span class="prismident">x2</span>&gt;<span class="prismnum">0</span> &amp; <span class="prismident">x2</span>&lt;<span class="prismnum">10</span> -&gt; <span class="prismnum">0.5</span>:(<span class="prismident">x1</span>'=<span class="prismnum">1</span>)&amp;(<span class="prismident">x2</span>'=<span class="prismident">x2</span>+<span class="prismnum">1</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">x1</span>'=<span class="prismnum">2</span>)&amp;(<span class="prismident">x2</span>'=<span class="prismident">x2</span>-<span class="prismnum">1</span>);<br/>
</div></div>
  <div class='sourceblocklink'><a href='Commands@action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Notice that elements of the updates are concatenated with <code>&amp;</code> and that each element must be bracketed individually.
If an update does not give a new value for a local variable, it is assumed not to change.
As a special case, the keyword <code><strong>true</strong></code> can be used to denote an update where no variable's value changes, i.e. the following are all equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>&gt;<span class="prismnum">10</span> | <span class="prismident">x2</span>&gt;<span class="prismnum">10</span> -&gt; (<span class="prismident">x1</span>'=<span class="prismident">x1</span>)&amp;(<span class="prismident">x2</span>'=<span class="prismident">x2</span>);<br/>
[] <span class="prismident">x1</span>&gt;<span class="prismnum">10</span> | <span class="prismident">x2</span>&gt;<span class="prismnum">10</span> -&gt; (<span class="prismident">x1</span>'=<span class="prismident">x1</span>);<br/>
[] <span class="prismident">x1</span>&gt;<span class="prismnum">10</span> | <span class="prismident">x2</span>&gt;<span class="prismnum">10</span> -&gt; <span class="prismkeyword">true</span>;<br/>
</div></div>
  <div class='sourceblocklink'><a href='Commands@action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Finally, it is important to remember that the expressions on the right hand side of each update refer to the state of the model <em>before</em> the update occurs. So, for example, this command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
  <div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>=<span class="prismnum">0</span> &amp; <span class="prismident">x2</span>=<span class="prismnum">1</span> -&gt; (<span class="prismident">x1</span>'=<span class="prismnum">2</span>)&amp;(<span class="prismident">x2</span>'=<span class="prismident">x1</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='Commands@action=sourceblock&amp;num=5' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>updates variable <code>x2</code> to 0, not 2.
</p>
<div class='vspace'></div>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Introduction.html'>The PRISM Language</a></strong>
</p><ul><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='Example1.html'>Example 1</a>
</li><li><a class='wikilink' href='ModelType.html'>Model Type</a>
</li><li><a class='wikilink' href='ModulesAndVariables.html'>Modules And Variables</a>
</li><li><a class='selflink' href='Commands.html'>Commands</a>
</li><li><a class='wikilink' href='ParallelComposition.html'>Parallel Composition</a>
</li><li><a class='wikilink' href='LocalNondeterminism.html'>Local Nondeterminism</a>
</li><li><a class='wikilink' href='CTMCs.html'>CTMCs</a>
</li><li><a class='wikilink' href='Example2.html'>Example 2</a>
</li><li><a class='wikilink' href='Constants.html'>Constants</a>
</li><li><a class='wikilink' href='Expressions.html'>Expressions</a>
</li><li><a class='wikilink' href='Synchronisation.html'>Synchronisation</a>
</li><li><a class='wikilink' href='ModuleRenaming.html'>Module Renaming</a>
</li><li><a class='wikilink' href='MultipleInitialStates.html'>Multiple Initial States</a>
</li><li><a class='wikilink' href='GlobalVariables.html'>Global Variables</a>
</li><li><a class='wikilink' href='FormulasAndLabels.html'>Formulas And Labels</a>
</li><li><a class='wikilink' href='PTAs.html'>PTAs</a>
</li><li><a class='wikilink' href='CostsAndRewards.html'>Costs And Rewards</a>
</li><li><a class='wikilink' href='ProcessAlgebraOperators.html'>Process Algebra Operators</a>
</li><li><a class='wikilink' href='PRISMModelFiles.html'>PRISM Model Files</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
